sends{-}msgs($s$;$v$;${\it tg\_f}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$map($\lambda$$x$.$\langle$1of(${\it tg\_f}$)$,\,$$x$$\rangle$;2of(${\it tg\_f}$)($s$,$v$))